package datatableaux;

import app.io.LoadWebFile;
import kb.DescriptionLogicsKB;
import entities.ConceptAssertion;
import entities.Individual;
import entities.concept.AndConcept;
import entities.concept.Concept;
import entities.concept.DomainConceptEQ;
import entities.concept.DomainConceptLT;
import entities.concept.DomainConceptLTEQ;
import entities.concept.ExistsConcept;
import entities.concept.NotConcept;
import entities.concept.OrConcept;
import entities.role.Role;
import entities.vocabulary.KBVocabulary;

public class TestReasoner {


	public static void main(String[] args){
		Reason res = new Reason(true);
		LoadWebFile loader = new LoadWebFile("http://localhost/kb/sample.kbox", false);
		loader.resolveFile();
		DescriptionLogicsKB kb= loader.getKB();
		Role gr= new Role("gender");
		Role ar = new Role("age");
		Role nr = new Role("name");
		Role sp = new Role("supervisedBy"); 
		DomainConceptEQ<?,?> d1 = new DomainConceptEQ<Role,String>(ar, "58");
		DomainConceptEQ<?,?> d2 = new DomainConceptEQ<Role,String>(nr, "prof_5");
		AndConcept ac = new AndConcept(d2,d1);
		Concept probc = new AndConcept(
				new DomainConceptLTEQ<Role,String>(ar, "28"),
				new NotConcept(new DomainConceptLT<Role,String>(ar, "01"))
				);
		ac = new AndConcept(ac, probc);
		Individual ind = Individual.newIndividual("ID00000002");
		ConceptAssertion lhs = new ConceptAssertion(ind, KBVocabulary.CONCEPT_TOP);
		ConceptAssertion rhs = new ConceptAssertion(ind, new ExistsConcept(sp, ac));
		res.ABoxUnionAssertionEntailAssertionCheck(lhs, rhs, kb);
	}
}
